Skip to main content

Derived preconditions and their use in program synthesis

Published 1982


Cover title

"March 1982"--Cover

"Prepared for: Naval Postgraduate School, Monterey, California 93940."

Includes bibliographical references (p. 25-26)

Technical report; 1982

In this paper we pose and begin to explore a deductive problem more general than that of finding a proof that a given goal formula logically follows from a given set of hypotheses. The problem is most simply stated in the propositional calculus: given a goal A and hypothesis H we wish to find a formula P, called a precondition, such that A logically follows from both P and H. A precondition provides any additional conditions under which A can be shown to follow from H. A slightly more complex definition of preconditions in a first-order theory is given and used throughout the paper. A formal system based on natural deduction is presented in which preconditions can be derived. A number of examples are then given which show how derived preconditions are used in a program synthesis method we are developing. These uses include theorem proving, formula simplification, simple code generation, the completion of partial specifications for a subalgorithm, and other tasks of a deductive nature. (Author)

ck/ 4/15/09

Publisher Monterey, California : Naval Postgraduate School
Pages 36
Language English
Call number ocm80333400
Digitizing sponsor Naval Postgraduate School, Dudley Knox Library
Book contributor Naval Postgraduate School, Dudley Knox Library
Collection navalpostgraduateschoollibrary; fedlink; americana

Full catalog record MARCXML

[Open Library icon]This book has an editable web page on Open Library.


There are no reviews yet. Be the first one to write a review.
Naval Postgraduate School, Dudley Knox Library
by Hixenbaugh, Milady Blaha.;Hixenbaugh, Paul Noel.
Source: half
Source: half